Other mathematical displays

The 19 environment can be used to set multi-line formulas without an enclosing box: it is useful for given-set declarations, theorems, and the miscellaneous bits of mathematics that don't come in a box:
#zed51#
is printed from the input

verbatim13#
The formula 20 may be abbreviated to 21; the 22 environment is a generalization of the 23 environment of LATEX, so this redefinition of commands is fairly benign. Notice that the maths is set flush left on the same indentation as schemas and their friends. Here too you can use 24 for a little extra space between lines.

For algebraic-style proofs, there is the 25 environment. This is like the 26 environment, but the separation between lines is increased a little, and page breaks may occur between lines. The intended use is for arguments like this:
#argue57#
Here, again, is the input:

verbatim14#
When the left-hand side is long, I find this style better than the LATEX 27 style, which wastes a lot of space.

Another brand of box is the inference rule; the rule
#infrule64#
comes from the input

verbatim15#
Note the optional argument to 28: it is a side-condition of the rule.

Finally, there's the 29 environment, used for making displays like this:
#syntax70#
from input like this:

verbatim16#
This kind of thing is useful when you're describing a language, and it can also be used for data-type definitions. I've even---time for a confession---used it once for a fragment of VDM. The final column is optional: just omit the third 30 if you don't want it.